/**
 * 
 */
package kodkod.analysis;

import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.Set;

import kodkod.ast.Formula;
import kodkod.ast.Relation;
import kodkod.ast.visitor.graph.GraphVisitorDOT;
import kodkod.engine.fol2sat.Translation;

/**
 * @author Markus Iser
 *
 */
public class AnalysisController {

	public static boolean CREATE_VAR_USAGE = false;
	public static boolean CREATE_AST_GRAPH = false;
	
	public static File varUsageFile = null;
	public static File astGraphFile = null;
		
	public static void enableVarUsageCreation() {
		CREATE_VAR_USAGE = true;
	}
	
	public static void disableVarUsageCreation() {
		CREATE_VAR_USAGE = false;
	}
	
	public static void setVarUsageFile(File file) {
		varUsageFile = file;
	}
	
	public static void enableAstGraphCreation() {
		CREATE_AST_GRAPH = true;
	}
	
	public static void disableAstGraphCreation() {
		CREATE_AST_GRAPH = false;
	}
	
	public static void setAstGraphFile(File file) {
		astGraphFile = file;
	}
	
	public static void performAnalysis(Translation translation, Formula formula) {
		if (CREATE_VAR_USAGE) {
			createVarUsage(translation);
		}
		if (CREATE_AST_GRAPH) {
			createAstGraph(formula);
		}
	}
	
	private static void createVarUsage(Translation translation) {
		try {
			File varUsage = varUsageFile;
			if (varUsage == null) File.createTempFile("Var", ".usage", new File(System.getProperty("java.io.tmpdir")));		
			BufferedWriter writer = new BufferedWriter(new FileWriter(varUsage));
			
			Set<Relation> keySet = translation.getPrimaryVarUsage().keySet();
			for (Relation rel : keySet) {
				int[] vars = translation.getPrimaryVarUsage().get(rel).toArray();
				writer.write(rel.name()+":");
				for (Integer var : vars) {
					writer.write(var+" ");
				}
				writer.write("\n");
			}
			writer.flush();
			writer.close();		
		} catch (IOException e) {
			e.printStackTrace();
		}
	}
	
	private static void createAstGraph(Formula formula) {
		GraphVisitorDOT graphVisitor;
		if (astGraphFile != null) {
			graphVisitor = new GraphVisitorDOT(astGraphFile);
		} else { 
			graphVisitor = new GraphVisitorDOT();
		}
        graphVisitor.visit(formula);
        graphVisitor.flush();
	}
}
